package kodkod.analysis;

import java.util.*;

import kodkod.ast.*;
import kodkod.ast.operator.ExprCastOperator;
import kodkod.ast.operator.IntOperator;
import kodkod.instance.TupleSet;

public class Casts extends HashSet<Expression> {
	
	public static boolean includeSumCasts = false;
	public static boolean includeNegCasts = false;
	
	public Casts(IntExpression exp) {
		super();
		
		if (exp instanceof UnaryIntExpression) {
			UnaryIntExpression e = (UnaryIntExpression)exp;
			if (includeNegCasts || !e.op().equals(IntOperator.NEG)) {
				this.addAll(new Casts(e.intExpr()));
			}
		} else if (exp instanceof BinaryIntExpression) {
			BinaryIntExpression e = (BinaryIntExpression)exp;
			this.addAll(new Casts(e.left()));
			if (includeNegCasts || !e.op().equals(IntOperator.MINUS)) {
				this.addAll(new Casts(e.right()));
			}
		} else if (exp instanceof NaryIntExpression) {
			NaryIntExpression e = (NaryIntExpression)exp;
			for (IntExpression child : e) this.addAll(new Casts(child));
		} else if (exp instanceof SumExpression) {
			SumExpression e = (SumExpression)exp;
			this.addAll(new Casts(e.intExpr()));
		} else if (exp instanceof IfIntExpression) {
			IfIntExpression e = (IfIntExpression)exp;
			this.addAll(new Casts(e.thenExpr()));
			this.addAll(new Casts(e.elseExpr()));
		} else if (exp instanceof ExprToIntCast) {
			ExprToIntCast e = (ExprToIntCast)exp;
			if (e.op().equals(ExprCastOperator.CARDINALITY)) {
				this.add(e.expression());
			} else if (includeSumCasts) {
				this.add(e.expression());
			}
		} 
//		else if (exp instanceof IntConstant) {} 
	}
}
